(* # ===================================================================
   # Matrix Project
   # Copyright FEM-NUAA.CN 2020
   # =================================================================== *)


Require Import Reals.
Open Scope R_scope.
Require Export Matrix.Mat.RMatrix.
Require Export Matrix.Mat.RMtacs.

(** * Sa -> Sg *)

(* φ   *)
Parameter phi   : R.

(* μ   *)
Parameter my    : R.

(* γ  *)
Parameter gamma : R.

(* 由 气流坐标轴系Sa 在OZ''Y''面转动 γ度  到 过度坐标轴系S’’ *)
Definition coordinate_transform_SaS'' : Mat R 3 3 := mkMat_3_3
  1         0          0
  0     (cos gamma) (-sin gamma)
  0     (sin gamma) (cos gamma ).

(* 由 过度坐标轴系S'' 飞机对称面转动 μ度  到 过度坐标轴系S’ *)
Definition coordinate_transform_S''S' : Mat R 3 3 := mkMat_3_3
  (cos my)    0  (sin my)
     0        1     0
  (- sin my)  0  (cos my).

(* 由 过度坐标轴系S’  在水平面转动 φ 度 到 地面坐标轴系Sg  *)
Definition coordinate_transform_S'Sg : Mat R 3 3 := mkMat_3_3
  (cos phi)   (-sin phi)  0
  (sin phi)   (cos phi)   0
     0           0        1.

Definition coordinate_transform_SaSg : Mat R 3 3 := mkMat_3_3
  ((cos my)*(cos phi)) ((sin my)*(cos phi)*(sin gamma)-(sin phi)*(cos gamma)) ((sin my)*(cos phi)*(cos gamma)+(sin phi)*(sin gamma))
  ((cos my)*(sin phi)) ((sin my)*(sin phi)*(sin gamma)+(cos phi)*(cos gamma)) ((sin my)*(sin phi)*(cos gamma)-(cos phi)*(sin gamma))
   ( -sin my)          ((cos my)*(sin gamma))                                 ((cos my)*(cos gamma)).

Definition transition_S'Sg_mul_S''S' : Mat R 3 3 := mkMat_3_3
  ((cos phi)*(cos my))  (-sin phi) ((cos phi)*(sin my))
  ((sin phi)*(cos my))   (cos phi ) ((sin phi)*(sin my))
   (-sin my)                 0          (cos my).

Lemma transition_S'Sg_mul_S''S'_eq:
  transition_S'Sg_mul_S''S' === RMmul coordinate_transform_S'Sg coordinate_transform_S''S'.
Proof.
  unfold transition_S'Sg_mul_S''S'.
  RMat_mul_simpl. unfold mkMat_3_3'.
  f_equal3.
Qed.

(* S'Sg_mul_S''S' * SaS'' = transition_S'Sg_mul_S''S' * SaS'' *)
Definition transition_S''Sb_mul_S'S''_mul_SgS' :=
  RMmul transition_S'Sg_mul_S''S' coordinate_transform_SaS''.


(* verify  S'Sg_mul_S''S' * SaS'' = SaSg *)
Lemma coordinate_transform_SaSg_eq :
  transition_S''Sb_mul_S'S''_mul_SgS' === coordinate_transform_SaSg.
Proof.
  unfold transition_S''Sb_mul_S'S''_mul_SgS',coordinate_transform_SaSg.
  RMat_mul_simpl. unfold mkMat_3_3'.
  f_equal2. ring. f_equal. ring. f_equal. ring.
  f_equal. ring. f_equal. ring. f_equal. ring.
Qed.